Nuprl Lemma : mapl_wf
11,40
postcript
pdf
A
,
B
:Type,
L
:(
A
List),
f
:({
a
:
A
| (
a
L
)}
B
). mapl(
f
;
L
)
(
B
List)
latex
Definitions
mapl(
f
;
l
)
Lemmas
map-wf2
origin
A, B:Type, L:(A List), f:({a:A| (a 
L)} 
B). mapl(f;L) (B List) A, B:Type, L:(A List), f:({a:A| (a L)} B). mapl(f;L) (B List)